FORMALISME ET FORMALISATION

FORMALISME ET FORMALISATION

Au sens moderne la formalisation est la présentation des théories scientifiques – et, en premier lieu sinon exclusivement, des mathématiques – dans le cadre d’un système formel , permettant de caractériser sans ambiguïté les expressions du langage et les règles de démonstration recevables.

On aurait tort de considérer pour autant que l’importance scientifique de la formalisation se réduise à une question de formulation. La formalisation des théories mathématiques fondamentales, suscitée à l’origine par les problèmes de «fondement» des mathématiques, a conduit tout au long du XX^e siècle au développement autonome d’une logique mathématique qui crée ses propres problèmes et concepts.

D’un autre côté, la formalisation des mathématiques est liée, dès son apparition, au développement de l’axiomatique et à l’étude des espèces de structures abstraites (selon la terminologie de Bourbaki), généralement «multivalentes», qui sont présentes dans les domaines les plus apparemment divers de la mathématique et en expliquent l’unité (structures algébriques surtout, à l’origine).

En ce sens, si le travail mathématique contemporain ne se déroule pas tout entier à l’intérieur d’un langage formalisé, on peut dire néanmoins qu’il met en évidence le formalisme, c’est-à-dire le caractère formel, de la connaissance mathématique.

L’idée de connaissance formelle

L’idée d’une connaissance formelle est en un sens aussi ancienne que la réflexion sur la science, c’est-à-dire que la philosophie. Mais c’est une idée aussi multivoque, et capable de transformations, que la catégorie même de forme, et que les couples de forme et matière, forme et contenu, forme et signification.

Les historiens de la logique, discutent toujours, à cet égard, sur l’interprétation de la syllogistique d’Aristote, de la logique stoïcienne des énoncés ou de la théorie médiévale des «conséquences». Mais ils s’accordent généralement à faire remonter quelques-unes des conceptions modernes sur la formalisation à la période classique et notamment à l’œuvre de Leibniz.

Le développement du calcul algébrique et de son symbolisme, l’explicitation des concepts de «relation» et de «fonction», sous-tendent, chez ce dernier, l’idée que le calcul, non seulement est la véritable forme du raisonnement rigoureux, mais peut s’étendre à d’autres objets que les grandeurs numériques. Leibniz établit le principe d’un calculus ratiocinator destiné à mécaniser les opérations du raisonnement logique; plus généralement, il concevait le projet d’exprimer toutes les idées dans une «caractéristique universelle» mettant en évidence symboliquement leurs relations de dépendance mutuelle et permettant de remplacer le travail de connaissance par le calcul analytique.

Il faut cependant remarquer que la pensée de Leibniz, pas plus que celle des logiciens antiques, n’est fondée sur la distinction de la forme et de la signification, puisqu’il veut représenter symboliquement les idées elles-mêmes et qu’il conçoit le raisonnement comme une analyse de leur compréhension, et en particulier la relation de conséquence logique comme une relation d’inclusion entre idées. On peut dire que – à la différence du projet hobbesien et condillacien de la science entendue comme «langue bien faite», «langue des calculs» –, la pensée de Leibniz, dont l’influence historique a été considérable, est un formalisme non empiriste lié à une conception spiritualiste de la forme, comme seule véritable substance.

Formalisme et logicisme

C’est au XIX^e siècle que se constitue véritablement la formalisation mathématique. Mais on peut dire schématiquement que sa genèse est partagée. D’un côté, elle procède du développement de l’algèbre abstraite et de l’extension de la notion de calcul dans le cadre d’une conception formaliste des mathématiques. De l’autre, elle devient le moyen nécessaire à l’analyse des concepts fondamentaux des mathématiques dans le cadre d’une philosophie logiciste.

La formalisation du calcul algébrique

Aux yeux des algébristes anglais (comme Peacock, De Morgan, Hamilton) et allemands (Grassmann, Hankel) du milieu du XIX^e siècle, la permanence du concept de nombre à travers ses extensions successives, qui n’est ni celle d’une représentation concrète, ni celle d’une évidence intellectuelle, est celle d’un symbolisme: le calcul sur les nombres complexes, sous réserve de définitions convenables des opérations algébriques, peut en effet s’écrire de la même façon que le calcul sur les entiers, les rationnels et les réels. Il obéit aux mêmes règles opératoires de commutativité, d’associativité et de distributivité ^{[cf. ALGÈBRE]}. Un système de «nombres» n’est donc pas autre chose qu’un système d’objets pour lesquels ces règles opératoires sont valides. Le concept de nombre, le concept des règles du calcul est en un sens un concept purement «logique». Il est important de noter que la «logique» ou «algèbre» de Boole représente précisément une extension de ce type. Or, on sait aujourd’hui qu’elle s’applique aussi bien au calcul des propositions qu’aux structures de réseaux électriques (ce qui en a fait un instrument privilégié de l’informatique).

Le point de vue qui s’exprime dans l’idée de calcul formel réduit par là le «sens» des concepts traditionnels aux règles de leur usage, et le distingue nettement d’une interprétation ou d’une représentation, réduites au statut d’«exemplification» et d’application. La mathématique formelle définit directement les structures opératoires «abstraites» et n’a aucun besoin d’en préciser d’abord l’interprétation intuitive, ce qui est une démarche extra-mathématique. De là un déplacement de l’objet de la science: celle-ci ne consiste pas à pratiquer et développer le calcul à son propre niveau, mais, puisque son essence réside en fait dans la mise en œuvre des règles, à définir, expliquer, et, éventuellement, varier et généraliser ces règles mêmes. Après avoir dégagé la notion générale de loi de composition, on élargit le champ de l’algèbre en définissant de nouveaux systèmes de «nombres» (par exemple les quaternions de Hamilton, définis par analogie avec les nombres complexes comme systèmes de quatre nombres réels, mais dont le produit n’est plus commutatif) et en construisant des calculs symboliques dont l’interprétation est tout à fait étrangère au domaine numérique (par exemple le calcul vectoriel, le calcul matriciel).

Ainsi, le formalisme apparaît comme capacité de créer des objets mathématiques nouveaux en définissant leur structure abstraite selon un mouvement que J. Cavaillès appelait le «moment de la variable, remplaçant les déterminations d’actes par la place vide pour une substitution».

Il permet d’unifier la mathématique en reconnaissant la structure des relations identiques dans lesquelles sont des «objets» d’ailleurs différents. Il conduit à définir la particularité «concrète» des notions mathématiques comme combinaison complexe de plusieurs structures de relations formelles. L’œuvre de N. Bourbaki a représenté en France, jusqu’à une date récente, l’aboutissement de ce point de vue.

Méthode axiomatique et formalisme

L’évolution de l’algèbre abstraite converge avec le développement de l’axiomatique, principalement issue de la réflexion sur la géométrie projective et les géométries non euclidiennes. Tout ce que le formalisme requiert pour s’autoriser à considérer un domaine d’objets mathématiques, c’est la non-contradiction logique des relations qui le définissent en quelque sorte implicitement. En revanche, il n’est nullement requis que ces relations aient un «sens intuitif», ou plutôt c’est le système des relations formelles, symboliquement exprimé, qui doit être considéré comme le sens.

De la même façon, dans les Grundlagen der Geometrie (1899), D. Hilbert montrait que le «sens» des propositions géométriques n’est aucunement lié aux représentations intuitives de l’espace, mais dépend seulement de la cohérence du système d’axiomes initial. Les notions primitives (point, droite, plan) à partir desquelles toutes les autres sont définies ne sont pas elles-mêmes définies: on peut considérer que les relations choisies comme axiomes les définissent implicitement.

Ici, on comprend mieux encore pourquoi le symbolisme n’est pas simplement un moyen d’expression commode ni une convention (même si, bien entendu, on peut toujours définir des symbolismes équivalents), mais tend à devenir l’objet même de la pensée et d’une véritable expérimentation mathématique. C’est le point de vue formel qui rend nécessaire, en pratique, le symbolisme: langage par construction exactement adéquat à une définition formelle, et susceptible d’être traité non pas comme un «moyen d’expression» renvoyant à un sens qu’il faudrait chercher et garder en mémoire, mais comme un nouvel objet, d’ailleurs matériel, et tout entier présent, exhibé aux yeux du théoricien.

Le logicisme

Il y a au contraire, au moins initialement, et sur le plan philosophique, une nette divergence entre la pensée formaliste et axiomatique (telle que la développe Hilbert) et le logicisme de G. Frege et B. Russell, second des grands courants qui sont à l’origine de la formalisation moderne.

Le projet de Frege, même s’il suppose la formalisation du raisonnement mathématique et la construction d’une écriture mathématique entièrement symbolique, est, à l’opposé du formalisme, un projet de réduction des mathématiques à la logique. Mais le terme «logique» n’a pas ici le même sens que tout à l’heure, où il s’agissait finalement de la non-contradiction d’un système de relations. Il désigne au contraire un ensemble de quelques notions considérées comme des termes universels intelligibles a priori de la pensée rationnelle, et inséparables de leur sens (bien que ce sens n’ait rien d’empirique). Telles sont, par exemple, les notions de concept, d’extension d’un concept c’est-à-dire de classe, et d’identité.

Selon Frege, le problème fondamental de l’arithmétique (le problème de ses fondements) est de construire une définition logique explicite du nombre entier qui mette en évidence son contenu de signification purement logique. Ce problème est en même temps le problème fondamental des mathématiques, dès lors que les méthodes d’arithmétisation de l’analyse élaborées par K. T. W. Weierstrass, R. Dedekind, G. Cantor permettent déjà de ramener les nombres réels, donc toutes les notions de l’analyse classique, à la notion de l’ensemble des entiers. Voici la définition de Frege, qui est une analyse en trois étapes de la notion de nombre:

«1. Le concept F est numériquement équivalent au concept G signifie qu’il existe une relation biunivoque entre les objets tombant sous le concept F et ceux qui tombent sous le concept G.

«2. Le nombre qui appartient au concept F est l’extension du concept numériquement équivalent à F.

«3. n est un nombre signifie il existe un concept tel que n soit le nombre qui lui appartient. »

La différence des deux points de vue, formaliste et logiciste, est plus apparente encore si on prend en considération l’œuvre de G. Boole, évoquée ci-dessus. Pour Boole, de façon typiquement formaliste, «la mathématique traite des opérations considérées en elles-mêmes, indépendamment des matières diverses auxquelles elles peuvent être appliquées». Les règles de la logique, qu’il s’agisse de la logique des enchaînements de propositions ou de la logique des classes, sont une telle matière, qu’il est possible de représenter par un calcul symbolique proche du calcul algébrique usuel. Le projet de Boole est une application de l’algèbre symbolique à la logique traditionnelle, une mathématisation de la logique, celui de Frege une logicisation des mathématiques.

Le contraste apparaît encore nettement dans les philosophies du langage qui s’étayent sur chacune des deux entreprises. On trouve chez Hilbert une réflexion sur la nature du signe matériel, dont la forme invariante permet la substitution dans les formules (qui comportent généralement plusieurs occurrences du «même» signe); et une réflexion sur la distinction des signes qui figurent dans les formules et de leur désignation dans une «métalangue» non formalisée permettant de définir les expressions formelles et les règles de leur dérivation. On trouve chez Frege une réflexion sur les concepts et les expressions du langage mathématique, envisagés comme des noms propres dont il faut caractériser les différents types de signification.

Cependant, l’entreprise logiciste ne pouvait être conduite qu’à la condition de transformer la logique traditionnelle en caractérisant de façon précise les formes propositionnelles qui peuvent apparaître dans la démonstration, et les règles d’inférence valides, donc en rendant la logique indépendante des représentations spontanées de la grammaire des langues naturelles. C’est ce que Frege entreprit le premier en construisant, dans sa Begriffschrift (1879), un système formel qu’il appliqua ensuite à la logicisation de l’arithmétique. Ultérieurement, il s’agit aussi d’éviter les contradictions ou les paradoxes que suscite l’emploi intuitif des notions logiques fondamentales (celle de classe ou d’ensemble).

La notion de système formel

La notion de système formel résulte finalement de la combinaison des deux courants, logiciste et formaliste, et peut être utilisée à titre de concept mathématique, de façon relativement indépendante des intentions philosophiques initiales.

On définit un système formel (ou théorie formalisée) en donnant une série de conditions.

La langue formalisée

1. On désigne explicitement un ensemble fini ou dénombrable de symboles, répartis selon leur usage en constantes, variables, symboles logiques, symboles de relations, symboles impropres (ponctuation, par exemple, dont l’usage pourrait être évité au moyen de conventions d’écriture). Une suite finie de symboles est appelée une expression du système.

2. On définit un sous-ensemble d’expressions du système, qu’on appelle les expressions correctement formées , ou formules du système. Intuitivement – mais la référence à l’intuition est étrangère à la problématique du logicien –, ces formules sont celles qui, dans une interprétation du système (en vue de laquelle il peut avoir été construit), ont une signification intelligible, représentant soit l’énoncé d’une relation, soit celui d’une proposition (qui peut être vraie ou fausse en logique «binaire», ou plus généralement prendre une «valeur de vérité » déterminée. C’est Wittgenstein qui, en définissant les «tables de vérité» du calcul des propositions, a ouvert la possibilité de déterminer axiomatiquement les valeurs de vérité).

Dans le cas général, il n’est pas possible d’énumérer effectivement toutes les formules, qui sont en nombre infini. On en donne une définition récursive , en énonçant des règles de formation dont l’application réitérée engendre les formules. Le plus souvent il existe alors un procédé purement mécanique permettant de décider effectivement si une expression donnée est une formule du système.

La démonstration formalisée

3. On définit un sous-ensemble de formules qu’on appelle les axiomes du système. Le plus souvent, on peut décider effectivement si une formule donnée est un axiome, et on parle alors de théorie axiomatique. Intuitivement, les axiomes représentent des propositions qui sont considérées comme vraies sans démonstration, mais cette référence est en toute rigueur inutile.

4. On définit une liste finie de relations R¹, ..., Rⁿ entre les formules, qu’on appelle règles d’inférence . Pour chaque règle Rⁱ , il existe un entier j bien déterminé tel que, pour tout ensemble de ^j formules et toute formule A, on puisse effectivement décider si les j formules considérées et la formule A sont dans la relation Rⁱ . Dans ce cas, on dit que A est une conséquence immédiate des formules considérées en vertu de Rⁱ .

On appelle démonstration formelle du système une suite finie de formules dont chacune est soit un axiome, soit une conséquence immédiate des formules précédentes en vertu d’une règle d’inférence. Une démonstration est dite démonstration de sa dernière formule. Un théorème du système est une formule dont il existe une démonstration. Intuitivement, les théorèmes sont les «vérités» de la théorie. Mais cette référence est absente de la définition d’un système formel, qui a justement pour but de représenter la notion de vérité par celle de démonstrabilité au sens qu’on vient d’indiquer.

Dans une théorie axiomatique formalisée, l’ensemble des théorèmes du système est défini de façon récursive, comme, précédemment, celui des formules correctes. Même lorsqu’une théorie formalisée est axiomatique, la notion de théorème n’y est cependant pas nécessairement «effective», c’est-à-dire qu’il n’est pas nécessairement possible de déterminer par un procédé mécanique si une formule quelconque donnée est un théorème. Lorsque c’est le cas, on parle de théorie «décidable»: c’est en somme un système formel tel qu’une machine convenablement construite puisse sélectionner tous les théorèmes (qu’on n’a donc pas besoin de «rechercher»). Cette notion est importante dans les applications techniques de la logique mathématique. Mais on montre que tous les systèmes formels suffisamment riches pour pouvoir représenter les théories mathématiques fondamentales sont en fait «indécidables».

L’ensemble des deux étapes, formalisation du langage, formalisation de la démonstration, constitue ce qu’on appelle quelquefois la construction de la syntaxe du système. Notion qui appartient, elle, à la «métalangue» du système.

La théorie de la formalisation

La construction de systèmes formels, dont on a vu qu’on peut chercher l’origine historique dans une tradition de philosophie mathématique aux aspects contradictoires, détermine historiquement un déplacement de la réflexion logique du plus grand intérêt épistémologique.

La formalisation des notions logiques qui sont en quelque sorte pratiquées implicitement dans le travail mathématique correspondait initialement à l’objectif de «fonder» la mathématique, ce qui est très clair dans la perspective logiciste de Frege et de Russell. Elle ne répondait pas à l’idée d’une transformation de l’objet de la logique comme science. Pourtant, la rupture est profonde avec une représentation traditionnelle parce que la formalisation expulse, au moins au niveau opératoire, la référence intuitive (l’évidence) des notions «logiques» mêmes, qui ne jouissent plus d’aucun privilège à cet égard. Un système formel simple peut servir à représenter la logique des propositions, l’ensemble des opérations logiques élémentaires qui réalisent la notion de conséquence: il suffit que les axiomes et les règles d’inférence règlent l’usage des symboles qu’on interprétera comme négation, implication, conjonction, disjonction. Mais il n’est généralement qu’une partie d’un système plus complexe, permettant de représenter en même temps la logique générale (c’est-à-dire la logique des prédicats ou relations) et des théories mathématiques comme la théorie des ensembles, l’arithmétique, la théorie des groupes, etc., ce qui suppose évidemment l’introduction d’axiomes spécifiques supplémentaires. Mais les axiomes «logiques» ne représentent alors qu’un sous-ensemble de l’ensemble des axiomes d’une théorie, qui sont situés sur le même plan et n’ont pas un usage différent dans la démonstration. On met ainsi clairement en évidence que l’ensemble des théorèmes, des vérités démontrées d’une théorie dépend simultanément des axiomes mathématiques et de la «logique» employée et peut varier en fonction des uns et de l’autre. On peut dire aussi que cette unification illustre le véritable rapport historique de la logique et des mathématiques : la logique ne «fonde» pas les progrès et les transformations historiques d’une mathématique qu’elle surplomberait du haut de sa validité universelle, de son éternité, de son évidence a priori. Elle est un aspect du travail mathématique qui en est entièrement solidaire.

Logique et mathématique

Cela ne signifie pas qu’il n’y ait aucun moyen de distinguer rigoureusement entre axiomes «logiques» et axiomes «mathématiques». Cette distinction est une question d’interprétation du système formel, c’est-à-dire de construction d’un modèle, ensemble d’objets mathématiques qui peuvent être mis en correspondance avec les symboles et les formules du système. À la suite des travaux de l’école polonaise (A. Tarski) et néo-positiviste (R. Carnap), on appelle généralement sémantique (par opposition à la syntaxe) l’étude théorique des modèles d’un système formel et de leurs propriétés.

En fait, l’objet de la logique théorique se trouve ainsi complètement déplacé, par un mouvement que Cavaillès nommait thématisation, posant comme nouvel objet le formalisme dans lequel on exprimait la théorie du précédent. La logique s’identifie dans ses problèmes, sinon dans ses objectifs, avec ce que Hilbert appelait la « métamathématique », c’est-à-dire la discipline (mathématique) qui, dans une « métalangue » rigoureuse, peut nous donner la connaissance scientifique de ces objets nouveaux que sont les «langues» et les systèmes axiomatiques formalisés. On se contentera ici de désigner les principaux de ces problèmes, en renvoyant le lecteur aux articles ou aux ouvrages spécialisés: problèmes de non-contradiction, de complétude (par rapport à un domaine d’interprétation donné), de «catégoricité» des systèmes formels (un système catégorique est un système dont tous les modèles sont isomorphes, c’est-à-dire mathématiquement indiscernables).

Parmi les résultats les plus remarquables, et qui illustrent le mieux le caractère d’imprévisibilité que la logique mathématique possède comme toute discipline scientifique, figurent les théorèmes dits de «limitation» des systèmes formels. Le plus célèbre est le théorème de Gödel (1931) énonçant l’incomplétude de l’arithmétique formalisée, c’est-à-dire la possibilité de construire une interprétation du système formel dans laquelle figure une proposition vraie qui est représentée dans le système par une expression formellement indémontrable. (Bien entendu la construction du système exclut la possibilité d’une formule démontrable qui correspondrait dans une interprétation quelconque à une proposition fausse; c’est même une condition du résultat précédent. La tentative de représenter la vérité des propositions de l’arithmétique par la démonstrabilité formelle n’aurait plus alors aucun sens cohérent.)

En quel sens avons-nous affaire ici à une «limitation»? Le résultat de Gödel montre que, pour une classe entière de systèmes formels, il faut renoncer à l’espoir d’une correspondance adéquate entre la notion sémantique de vérité (qui n’a de sens que pour une interprétation du système) et la notion purement syntaxique de démonstrabilité. Et comme l’interprétation d’un système est réglée par les propriétés syntaxiques du système lui-même, cela signifie que la syntaxe du système autorise la définition d’une notion de «vérité» qu’elle est cependant impuissante à représenter exactement.

Dans une perspective idéaliste (par exemple celle qu’adoptait Husserl lorsqu’il définissait la «clôture» formelle comme l’idéal régulateur de toute science théorique), ce résultat est ressenti comme une déception . Il permet d’étayer sur le développement même de la logique mathématique une philosophie de la finitude de la connaissance humaine.

Dans une perspective matérialiste, ce résultat, comme l’ensemble des théorèmes de «limitation», est interprété positivement . Il exprime une propriété structurale fondamentale des systèmes formels considérés. Il ne borne donc pas la connaissance que ceux-ci représentent : il étend au contraire notre connaissance de ce qu’ils sont . Sa seule fonction négative est celle, critique, de faire obstacle sur ce terrain à une philosophie du savoir absolu.

Formalisation et connaissance

L’histoire de la formalisation met en évidence la réalisation par les mathématiques d’une idée de la connaissance formelle qu’elles ne peuvent s’approprier effectivement sans la transformer. Mouvement caractéristique du travail scientifique, qui porte seulement ici sur un problème plus traditionnellement investi que d’autres par la philosophie.

Si les mathématiques en viennent historiquement à se définir comme une connaissance formelle, c’est-à-dire formalisée ou formalisable, on poserait volontiers un problème réciproque, qu’on pourrait appeler par analogie un problème de «complétude»: ne s’agit-il pas du caractère spécifiquement mathématique de la connaissance? La question doit être posée par référence à la physique, où la mathématique n’est couramment considérée que comme un langage , appliqué à la construction de «modèles» de la réalité matérielle (en un sens inverse de celui qu’on a rencontré plus haut à propos de la sémantique des systèmes formels).

Elle doit être posée par référence à la linguistique, qui présente la même situation épistémologique dans certaines de ses branches récentes. Mais, surtout, une discipline comme la phonologie structurale (fondée par R. Jakobson et N. S. Troubetzkoï entre 1920 et 1930) semble procéder sur son propre terrain à une transformation spécifique de l’idée de connaissance formelle. Du moins est-ce ainsi qu’on peut interpréter la définition du système phonologique d’une langue comme système d’oppositions entre phonèmes, et la définition du phonème comme système de traits distinctifs pertinents. Plus récemment, les travaux de N. Chomsky et de son école ont étendu les procédures algébriques à l’étude des structures syntaxiques des «langues naturelles». À leur tour, des mathématiciens comme R. Thom ont tenté d’intégrer la linguistique formelle dans une théorie générale des systèmes et de leurs conditions d’équilibre. D’où une résurgence (qui ne fait pas l’unanimité) des problèmes philosophiques de «grammaire universelle» (à la manière de Leibniz) et de «catégories de l’esprit humain» (à la manière de Kant).

Dans un cas comme dans l’autre, la formalisation pose en fait à l’épistémologie la question de son articulation avec la science expérimentale. Une œuvre épistémologique comme celle de Bachelard est tout entière consacrée, précisément, à analyser la combinaison dialectique des réalisations expérimentales et de la formalisation mathématique dans la science contemporaine, et à démontrer le rôle constitutif, générateur de connaissances nouvelles, de la formalisation. À la même époque, L. Wittgenstein, dont le Tractatus logico-philosophicus avait été interprété par le positivisme logique comme la fondation d’une technique «rigoureuse» de réduction des concepts scientifiques à la combinaison des formalismes logico-mathématiques et d’«observables» empiriques, engageait dans ses Investigations philosophiques une déconstruction systématique de ce nouveau dogmatisme. Il montrait, dans les contradictions de l’usage , dans la multiplicité des «jeux de langage» et les effets différentiels des pratiques signifiantes, la condition même de la connaissance. Dès lors la formalisation ne vaut pas seulement par la «garantie» de cohérence relative qu’elle procure, mais aussi par les conflits internes qui caractérisent son historicité.

On verra donc dans le formalisme – qu’il y a intérêt à distinguer clairement de la formalisation, par-delà les fréquentes oscillations de la terminologie – une philosophie, ou plutôt une tendance philosophique, parmi d’autres positions philosophiques affrontées en fonction du développement de la formalisation scientifique.

Encyclopédie Universelle. 2012.